a:rationals. qle(a; a) 

latex

Definitions	P  Q, T, (i = j), qeq(r; s), ff, i <z j, tt, r - s, qpositive(r), bor(p; q), q_le(r; s), qadd_grp, t.2, t.1, grp_le(g), x f y, if b then t else f fi , b, grp_leq(g; a; b), r * s, r + s, t  T, P  Q, prop{i:l}, P  Q, True, P  Q, qle(r; s), x:A. B(x), guard(T), subtype(S; T)
Lemmas	qinverse q, qadd comm q, rationals wf, squash wf, qadd preserves qle, true wf, int inc rationals, qmul wf, qadd wf, qle wf, iff transitivity